(* # =================================================================== 
   # Introduction
   #
   # This file is for the proof of the axioms used in FDPIA_build.v.
   #
   # The denotation semantics of primitives are defined in a state-based model
   #
   # Types: data,exp,acc,env,comm
   #
   # Functional Primitives: mapSeq mapPar reduce zip split join
   #
   # Imperative Primitives: skip seq seqfor parfor assign new
   #
   # Imperative Micros: mapSeql mapParl reducel
   #
   # Function about env: vrd vrm
   #
   # Lemmas for Optimization Rules:
   #
   # 1. mapPar_mapPar: forall [n:nat] [d1 d2 d3:data] 
   #    (f:exp d1 -> exp d2) (g: exp d2 -> exp d3) (v:exp (ary '{n} d1)),
   #    mapPar g (mapPar f v) = mapPar (fun i => g (f i)) v.
   #
   # 2. mapPar_join_split: forall [m n:nat] [d1 d2:data] (f:exp d1 -> exp d2) (v:exp (ary '{m*n} d1)),
   #    mapPar f v = join (mapPar (mapPar f) (split v)).
   #
   # 3. reduce_mapSeq: forall [n:nat] [d1 d2 d3:data] (g:exp d1 -> exp d2) 
   #    (f: exp d2 -> exp d3 -> exp d3) (i:exp d3)(v:exp (ary '{n} d1)),
   #    reduce f i (mapSeq g v) = reduce (fun x a => f (g x) a) i v.
   #
   # 4. join_split: forall (m n:nat) (d:data) (v: exp (ary '{m*n} d)),
   #    join (split v) = v.
   #
   # 5. split_join: forall (m n:nat) (d:data) (v: exp (ary '{m} (ary '{n} d))),
   #    split (join v) = v.
   #
   # 6. product_eq: forall (m n:nat) (a b: exp(ary '{m*n} num)),
   #    reduce add zero (mapPar (cur mul) (zip a b)) =
   #    reduce add zero(join (mapPar (mapPar (cur mul)) (split (zip a b)))).
   #
   # 7. zip_mapPar: forall (d1 d2:data) (n:nat) (f g: exp d1 -> exp d2) (a b: exp (ary '{n} d1)),
   #    zip (mapPar f a) (mapPar g b) = mapPar (fun xy => (f (Fst xy),g (Snd xy)): exp (tensor d2)) (zip a b).
   #
   # Auxiliary Lemmas：
   #
   # 1. assign_vrd: forall d (a:path) eta, ((@acc' d a) |:= (vrd eta (acc' a))) eta = eta.
   # 2. vrd_assign: forall d (a1:path) (a2:path) (e:exp d) eta,
   #    vrd (((acc' a1)|:= e) eta) (acc' a2) = if path_eqb a1 a2 then e else vrd eta (acc' a2).
   # 3. vrm_assign: forall d (a:path) (e:exp d) eta,
   #    @vrm d (acc' a) (assign (acc' a) e eta) = eta.
   # 4. assign_assign: forall d (a1 a2:path) (e1 e2:exp d) eta,
   #    (acc' a1 |:= e1) ((acc' a2 |:= e2) eta) = 
   #    if a1 =? a2 then acc' a1 |:= e1 eta else (acc' a2 |:= e2) ((acc' a1|:= e1) eta) .
   # 5. seqfor_add: forall (m n:nat) (f: fin (n+m) -> comm),
   #    seqfor (fun i : fin (n + m) => f i) =
   #    seqfor (fun i : fin m => f (nat2fin (n+m) (i))) '; seqfor (fun (j : fin n) => f (nat2fin (n+m) (j+m))).
   # 6. seqfor_nested : forall m n (f:fin m -> fin n -> comm),
   #    seqfor (fun (i: fin m) => seqfor (fun (j:fin n) => f i j))
   #    = seqfor (fun (i: fin (m*n)) => f (nat2fin m (i/n)) (nat2fin n (i mod n))).
   #
   # Lemmas for the axioms in FDPIA_build.v:
   #
   #  Lemma new_equiv: forall d (c: exp d -> comm) (e1:exp d)(a:path)  ,
   #    (forall e e1 x, c e1 (((acc' a) |:= e) x) = ((@acc' d a)|:= e) (c e1 x)) ->
   #    @new d (fun a0 => a0 |:= e1 '; (fun eta => c (vrd eta a0) eta)) (acc' a) = c e1 .
   #
   #  reducel_equiv: forall n d1 d2 (f:exp d1 -> exp d2 -> exp d2) (i:exp d2) (a a1:path) (e:exp (ary '{n} d1)) , a<>a1 ->
   #    (acc' a) |:= reduce f i e = @new d2 (fun a0 =>  a0 |:= i ';
   #    @seqfor n (fun (i0: fin n) eta => (a0 |:= f e |[ i0] (vrd eta a0)) eta) ';
   #    fun eta => ((acc' a) |:= (vrd eta a0)) eta) (acc' a1).
   #
   #  assign_ary_par: forall m (n : fle m) (d : data) (a : path) (x : exp (ary n d)),
   #    acc' a |:= x = parfor (fun (i: fin n) (o : acc d) => o |:= x |[i]) (@acc' (ary n d) a).
   #
   #  assign_tensor: forall (d : data) (a : path) (x : exp (tensor d)), 
   #    (acc' a) |:= x = pairAcc1 (acc' a) |:= Fst x '; pairAcc2 (acc' a) |:= Snd x.
   #
   #  assign_pair: forall (d : data) (e1 e2 : exp d) (a : path),
   #    acc' a |:= Pair e1 e2 = pairAcc1 (acc' a) |:= e1 '; pairAcc2 (acc' a) |:= e2.
   #
   #  mapSeq_equiv : forall m (n : fle m) (d1 d2 : data) (f : exp d1 -> exp d2) (v:exp (ary n d1)) (a :path),
   #    @acc' (ary n d2)  a |:= mapSeq f v  = seqfor (fun i : fin n => (@acc' (ary n d2)  a)|{i} |:= f v|[i]).
   #
   #  mapPar_equiv : forall m (n : fle m) (d1 d2 : data) (f : exp d1 -> exp d2) (v:exp (ary n d1)) (a : path),
   #    @acc' (ary n d2) a |:= mapPar f v  = parfor (fun (i : fin n) o => o |:= f v|[i]) (@acc' (ary n d2) a ).
   #
   #  zip_equiv : forall m (n:fle m) d (a: path) (e1 e2:exp(ary n d)), 
   #    @acc' (ary n (tensor d)) a |:= zip e1 e2 
   #    = zipAcc1 (@acc' (ary n (tensor d)) a) |:= e1 '; zipAcc2 (@acc' (ary n (tensor d)) a) |:= e2.
   #
   #  split_equiv: forall (m n : nat) (d : data) (e : exp (ary '{ m * n} d)) (a : path),
   #    acc' a |:= split e = splitAcc (acc' a) |:= e.
   #
   #  join_equiv: forall (n m : nat) (d : data) (e : exp (ary '{ m} (ary '{ n} d))) (a : path),
   #    acc' a |:= join e = joinAcc (acc' a) |:= e.
   #
   #  reducel_equiv2:forall (n : nat) (d1 d2 : data) (f : exp d1 -> exp d2 -> exp d2) 
   #    (i : exp d2) (e : exp (ary '{ n} d1)) (c : exp d2 -> comm) (a:path),
   #    (forall e e1 x, c e1 (((@acc' d2  a) |:= e) x) = ((@acc' d2 a)|:= e) (c e1 x)) ->
   #     c (reduce f i e) = new (fun ac => ac |:= i '; seqfor (fun (i0 : fin n) eta => 
   #     (ac |:= f e |[ i0] (vrd eta ac)) eta) '; (fun eta => c (vrd eta ac) eta)) (acc' a).
   #
   # =================================================================== *)


Require Import Logic.FunctionalExtensionality.
Require Import List Reals String.
Import ListNotations.
Require Export finType vector CpdtTactics.
Set Implicit Arguments.
Hint Unfold v_map v_zip v_idx v_split v_join.

(* ************************* Types ************************* *)

Inductive data : Set := 
  | num   : data
  | ary   : forall (n:nat), fle n-> data -> data   
  | tensor: data -> data.

Fixpoint exp (d:data) : Set :=
  match d with
  | num => R 
  | ary n d => vector (exp d) n
  | tensor d => (exp d) * (exp d)
  end.

(* the default value of every exp *)
Fixpoint exp_default (d:data) : exp d :=
  match d with
  | num => 0%R
  | ary n d => v_make n (exp_default d)
  | tensor d => (exp_default d, exp_default d)
  end.

Fixpoint data_eqb (d1 d2:data):bool :=
  match d1,d2 with
  | num , num => true
  | @ary n1 m1 d3,@ary n2 m2 d4 => andb (n1 =? n2) (andb (m1 =? m2) (data_eqb d3 d4))
  | tensor d1 , tensor d2 => (data_eqb d1 d2)
  | _,_ => false
  end.

Inductive path :=
  | Var : string -> path
  | AryIdx (n:nat) (i:fin n)  : path -> path
  | PairL : path -> path
  | PairR : path -> path . 

Fixpoint path_eqb (p1 p2: path) : bool :=
  match p1,p2 with
  | Var p3 , Var p4 => String.eqb p3 p4
  | AryIdx n1 i1  p3 , AryIdx n2 i2 p4 => 
    andb (Nat.eqb n1 n2) (andb (Nat.eqb i1 i2) (path_eqb p3 p4))
  | PairL p3 , PairL p4 => path_eqb p3 p4
  | PairR p3 , PairR p4 => path_eqb p3 p4
  | _ , _ => false
  end.

Declare Scope path_scope.
Infix "=?" := path_eqb : path_scope.
Open Scope path_scope.

Lemma path_eqb_refl : forall (p: path),
  p =? p = true.
Proof.
  induction p;crush.
  - apply eqb_refl. - rewrite ?Nat.eqb_refl; auto.
Qed.

Lemma AryIdx_eq: forall (n1 n2:nat) (i1: fin n1) (i2:fin n2)
  (p1 p2: path), n1 = n2 ->
  Nat.eq i1 i2 -> p1 = p2 ->
  AryIdx n1 i1 p1 = AryIdx n2 i2 p2.
Proof.
  intros. subst. f_equal. apply fin_eq. auto.
Qed.

Lemma AryIdx_eq_r: forall (n1 n2:nat) (i1: fin n1) (i2:fin n2)
  (p1 p2: path), 
  AryIdx n1 i1 p1 = AryIdx n2 i2 p2 ->
  (n1 = n2 /\ fin2nat i1 = fin2nat i2 /\ p1 = p2).
Proof.
  intros. inversion H. split. auto. split. auto. auto.
Qed.

Ltac andb_red H:=
  apply Bool.andb_true_iff in H;inversion H;clear H.

Lemma path_eqb_eq: forall (p1 p2:path),
  p1 = p2 <-> p1 =? p2 = true.
Proof.
  intros. split;intros;subst. apply path_eqb_refl.
  generalize dependent p2. generalize dependent p1.
  induction p1,p2; crush; f_equal;try (apply eqb_eq);auto. 
  - andb_red H. andb_red H1. 
    apply AryIdx_eq;try apply Nat.eqb_eq;auto.
Qed.

Lemma path_eqb_neq : forall (p1 p2:path),
  p1 <> p2 <-> p1 =? p2 = false.
Proof.
  induction p1,p2;crush;
  try(apply IHp1; intros; apply H; subst;auto);
  try(rewrite path_eqb_refl in H;discriminate).
  - apply eqb_neq; red;intros; apply H. subst;auto.
  - rewrite eqb_refl in H; discriminate.
  - destruct (n =? n0)%nat eqn:E;
    destruct (i =? i0)%nat eqn:E1;simpl; auto. apply IHp1.
    intros; apply H. apply Nat.eqb_eq in E,E1; subst.
    apply AryIdx_eq;auto.
  - apply AryIdx_eq_r in H0. inv H0. inv H2. subst. 
    rewrite ?Nat.eqb_refl,path_eqb_refl in H; simpl in H.
    rewrite Bool.andb_true_r in H. rewrite H3 in H. 
    rewrite Nat.eqb_refl in H; discriminate.
Qed.

Lemma path_eqb_sym : forall (p1 p2: path) (b:bool),
  p1 =? p2 = b -> p2 =? p1 = b.
Proof.
  induction b;intros. apply path_eqb_eq in H. rewrite H. apply path_eqb_refl.
  apply path_eqb_neq in H. apply path_eqb_neq. auto.
Qed. 

Fixpoint acc (d:data) : Set :=
  match d with
  | num => path 
  | ary n d => vector (acc d) n
  | tensor d => (acc d) * (acc d)
  end.

Fixpoint acc' {d:data} (p:path) : acc d:=
  match d with
  | num => p:acc num
  | @ary n m d1 => mk_vec (fun i => acc' (AryIdx n (nat2fin n i) p))
  | tensor d1 => (acc' (PairL p),acc' (PairR p))
  end.
   
Fixpoint acc_default (d:data) : acc d :=
  match d with
  | num => Var ""
  | ary n d => v_make n (acc_default d)
  | tensor d => (acc_default d, acc_default d)
  end.

Notation " '{ n } " := (fle_self n) (at level 2).

(* ****************** Functional Primitives ****************** *)

(* Primitives for Scalar Expression *)
Definition negate : exp num -> exp num:= Ropp.
Definition add : exp num -> exp num -> exp num := Rplus.
Definition mul : exp num -> exp num -> exp num := Rmult.
Definition zero : exp num := 0%R.
Definition one : exp num := 1%R.

(* Primitives for Array Expression *)
Definition reduce {n:nat} {d1 d2:data} (f:(exp d1)->(exp d2)->(exp d2)) (init:exp d2) (v:exp (ary '{ n } d1)):=
  v_reduce f init v.
Definition mapPar {n:nat} {d1 d2:data} (f:exp d1 -> exp d2) (v:exp (ary '{ n } d1)) : exp (ary '{ n } d2):=
  v_map (exp_default d1) f v.
Definition mapSeq {n:nat} {d1 d2:data} (f:exp d1 -> exp d2) (v:exp (ary '{ n } d1)) : exp (ary '{ n } d2):=
  v_map (exp_default d1) f v.
Definition zip {n:nat} {d:data} (v1 v2:exp (ary '{ n } d)) : exp (ary '{ n } (tensor d)):=
  v_zip (exp_default d) (exp_default d) v1 v2.
Definition idx {n:nat} {d:data} (v:exp (ary '{ n } d)) (i:fin n) := v_idx (exp_default d) v i.
Definition split {d:data} {n m:nat} (v:exp(ary '{ m*n } d)) : exp (ary '{ m } (ary '{ n } d)) :=
  v_split (exp_default d) v.
Definition join {d:data} {n m:nat} (v: exp (ary '{ m } (ary '{ n } d))) : exp(ary '{ m*n } d) :=
  v_join (exp_default d) (exp_default (ary '{n} d)) v.

Notation " e |[ i ] " := (idx e i) (at level 2).

(* Primitives for Dual Expression *)
Definition Pair {d:data} (v1 v2: exp d) : exp (tensor d):= pair v1 v2.
Definition Fst {d:data} (v :exp (tensor d)) : exp d := fst v.
Definition Snd {d:data} (v :exp (tensor d)) : exp d := snd v.

(* Primitives for Array Acceptor *)
Definition zipAcc1 {n:nat} {d:data} (v : acc (ary '{ n } (tensor d))) : acc (ary '{ n } d):= v_unzip1 (acc_default (tensor d)) v.
Definition zipAcc2 {n:nat} {d:data} (v : acc (ary '{ n } (tensor d))) : acc (ary '{ n } d) := v_unzip2 (acc_default (tensor d)) v.
Definition idxAcc {n:nat} {d:data} (v:acc (ary '{ n } d)) (i:fin n) := v_idx (acc_default d) v i.
Definition splitAcc {d:data} {n m:nat} (v: acc (ary '{ m } (ary '{ n } d))) :acc(ary '{ m*n } d):=
  v_join (acc_default d) (acc_default (ary '{n} d)) v.
Definition joinAcc {d:data} {n m:nat} (v: acc(ary '{ m*n } d)) : acc (ary '{ m } (ary '{ n } d)) :=
  v_split (acc_default d) v.

Notation " a |{ i } " := (idxAcc a i) (at level 2).

(* Primitives for Dual Acceptor *)
Definition pairAcc1 (d:data) (v : acc (tensor d)) : acc d := fst v.
Definition pairAcc2 (d:data) (v : acc (tensor d)) : acc d := snd v.

Definition cur {d d1:data} (f: exp d -> exp d -> exp d1):=
  fun (xy:exp (tensor d)) => f (Fst xy) (Snd xy).

Hint Unfold reduce mapPar mapSeq zip idx split join 
  zipAcc1 zipAcc2 idxAcc splitAcc joinAcc.

(* ****************** Optimization Rules ****************** *)

Lemma mapPar_mapPar: forall [n:nat] [d1 d2 d3:data] 
  (f:exp d1 -> exp d2) (g: exp d2 -> exp d3) (v:exp (ary '{n} d1)),
  mapPar g (mapPar f v) = mapPar (fun i => g (f i)) v.
Proof. intros. apply v_map_fg. Qed.

Lemma mapPar_join_split: forall [m n:nat] [d1 d2:data] (f:exp d1 -> exp d2) (v:exp (ary '{m*n} d1)),
  mapPar f v = join (mapPar (mapPar f) (split v)).
Proof. intros. apply v_map_join_split. Qed.

Lemma reduce_mapSeq: forall [n:nat] [d1 d2 d3:data] (g:exp d1 -> exp d2) 
    (f: exp d2 -> exp d3 -> exp d3) (i:exp d3)(v:exp (ary '{n} d1)),
  reduce f i (mapSeq g v) = reduce (fun x a => f (g x) a) i v.
Proof. intros. apply v_reduce_map. Qed. 

Lemma join_split: forall (m n:nat) (d:data) (v: exp (ary '{m*n} d)),
  join (split v) = v.
Proof. intros. apply v_join_split. Qed.

Lemma split_join: forall (m n:nat) (d:data) (v: exp (ary '{m} (ary '{n} d))),
  split (join v) = v.
Proof. intros. apply v_split_join. Qed.

Lemma product_eq: forall (m n:nat) (a b: exp(ary '{m*n} num)),
  reduce add zero (mapPar (cur mul) (zip a b)) =
  reduce add zero(join (mapPar (mapPar (cur mul)) (split (zip a b)))).
Proof. intros. rewrite mapPar_join_split. auto. Qed.

Lemma zip_mapPar: forall (d1 d2:data) (n:nat) (f g: exp d1 -> exp d2) (a b: exp (ary '{n} d1)),
  zip (mapPar f a) (mapPar g b) = mapPar (fun xy => (f (Fst xy),g (Snd xy)): exp (tensor d2)) (zip a b).
Proof. intros. apply v_zip_map. Qed.

(* ****************** Environment ****************** *)

Definition env := path -> exp num. 

Definition env_empty (v:exp num) :env :=
   fun _ => v.

Definition update (m : env) (x : path)(v : exp num) :=
  fun x' => if path_eqb x x' then v else m x'.

Parameter remove: path -> env -> env.

Axiom remove_update: forall (x:path) (e:exp num) (m:env),
  remove x (update m x e) = m. 

Notation "'_' '!->' v" := (env_empty v)
  (at level 100, right associativity).

Notation "x '!->' v ';' m" := (update m x v)
  (at level 100, v at next level, right associativity).

Lemma update_eq : forall (m : env) x v,
  (x !-> v ; m) x = v.
Proof.
  unfold update. intros. rewrite path_eqb_refl;auto.
Qed.

Theorem update_neq : forall (m : env) x1 x2 v,
  x1 <> x2 ->
  (x1 !-> v ; m) x2 = m x2.
Proof.
  intros. unfold update. apply path_eqb_neq in H.
  rewrite H. auto.
Qed.

Lemma update_shadow : forall (m : env) x v1 v2,
  (x !-> v2 ; x !-> v1 ; m) = (x !-> v2 ; m).
Proof.
  intros. unfold update. fun_ext. destruct (x=?x0).
  auto. auto.
Qed.

Theorem update_same : forall (m : env) x,
  (x !-> m x ; m) = m.
Proof.
  unfold update. intros. fun_ext. destruct (x=?x0) eqn:E.
  apply path_eqb_eq in E. rewrite E. auto. auto.
Qed.

Theorem update_permute : forall (m : env) v1 v2 x1 x2,
  x2 <> x1 ->
  (x1 !-> v1 ; x2 !-> v2 ; m) = (x2 !-> v2 ; x1 !-> v1 ; m).
Proof.
  intros. unfold update. fun_ext. destruct (x1=?x) eqn:E.
  apply path_eqb_eq in E. subst. apply path_eqb_neq in H.
  rewrite H. auto. auto.
Qed.

(* ****************** Command ****************** *)

Definition comm:= env -> env.

Definition skip :comm:= fun (eta:env) => eta.

Definition seq (p1 p2:comm):comm:= 
  fun (eta:env) => p2 (p1 eta).

Notation " p1 '; p2 " := (seq p1 p2) (right associativity,at level 65).

Fixpoint seqfor {m:nat} : (fin m -> comm) -> comm :=
  match m with
  | O => fun (_ :_ )=> skip
  | S m' => fun (p: fin (S m') -> comm) =>
     seqfor (fun i => p (fin2finS i)) ';
     p (exist _ m' (Nat.lt_succ_diag_r m'))
  end.

Lemma seqfor_Sn: forall (m:nat)(p: fin (S m) -> comm),
  seqfor p = 
    seqfor (fun i => p (fin2finS i)) ';
    p (exist _ m (Nat.lt_succ_diag_r m)).
Proof. auto. Qed.

Lemma seqfor_no_change: forall (m:nat) eta,
  seqfor (fun (i:fin m) (eta:env) =>  eta) eta = eta.
Proof. induction m;auto. Qed.

Lemma seqfor_mul_0: forall (m:nat) (p: fin (m*0) -> comm) eta,
  seqfor p eta = eta.
Proof.
  induction m;auto.
Qed.

Lemma seqfor_0: forall (p: fin 0 -> comm) eta,
  seqfor p eta = eta.
Proof. auto. Qed.

Lemma seqfor_add: forall (m n:nat) (f: fin (n+m) -> comm),
  seqfor (fun i : fin (n + m) => f i) =
  seqfor (fun i : fin m => f (nat2fin (n+m) (i))) '; seqfor (fun (j : fin n) => f (nat2fin (n+m) (j+m))).
Proof. unfold seq.
  induction m. 
  - intro n. replace (n+0) with n;auto. intros. fun_ext. induction n;auto.
    f_equal. fun_ext. f_equal. apply fin_eq. autorewrite with core. auto. rewrite Nat.add_0_r;auto.
  - induction n. * replace (0 + S m) with (S m) ;auto. intros. fun_ext. rewrite seqfor_0. f_equal.
    fun_ext. f_equal. apply fin_eq. autorewrite with core;auto. 
    * simpl(S n + S m). intros. fun_ext. rewrite ?seqfor_Sn. unfold seq. f_equal. autorewrite with core.
      unfold nat2fin. destruct (le_lt_dec (S (n + S m)) (n + S m)). lia. f_equal. apply lt_unique.
      rewrite IHn.
      replace (seqfor (fun j : fin n => f (fin2finS (nat2fin (n + S m) (j + S m))))) with
      (seqfor (fun i : fin n => f (nat2fin (S (n + S m)) (fin2finS i + S m)))). f_equal.
      rewrite seqfor_Sn. unfold seq. f_equal. apply fin_eq. autorewrite with core;auto. lia. lia.
      induction m;auto. f_equal. fun_ext. f_equal. apply fin_eq;autorewrite with core;auto.
      induction x0;simpl. lia. induction x0; simpl. lia. 
      induction n;auto. f_equal. fun_ext. f_equal. apply fin_eq;autorewrite with core;auto.
      induction x0;simpl. lia. induction x0; simpl. lia. 
Qed.

Lemma seqfor_nested : forall m n (f:fin m -> fin n -> comm),
  seqfor (fun (i: fin m) => seqfor (fun (j:fin n) => f i j))
  = seqfor (fun (i: fin (m*n)) => f (nat2fin m (i/n)) (nat2fin n (i mod n))).
Proof.
  induction m;auto.
  induction n. simpl. intros. fun_ext. unfold seq,skip. rewrite seqfor_mul_0,seqfor_no_change. auto.
  intros. simpl (S m * S n). rewrite ?seqfor_Sn. unfold seq.  fun_ext.  
  f_equal. * autorewrite with core. replace ((n + m * S n) / S n) with m.
  unfold nat2fin. destruct(le_lt_dec (S m) m). lia. f_equal. apply lt_unique.
  rewrite Nat.div_add,Nat.div_small;auto. 
  * replace (@fin2nat (S (Init.Nat.add n (Init.Nat.mul m (S n))))
           (@exist nat (fun i : nat => lt i (S (Init.Nat.add n (Init.Nat.mul m (S n)))))
              (Init.Nat.add n (Init.Nat.mul m (S n))) (Nat.lt_succ_diag_r (Init.Nat.add n (Init.Nat.mul m (S n)))))) 
    with (n + m * S n) . replace ((n + m * S n) mod S n) with n. unfold nat2fin.
  destruct (le_lt_dec (S n) n). lia. f_equal. apply lt_unique.
  rewrite Nat.mod_add,Nat.mod_small;auto. auto.
  * rewrite IHm. rewrite seqfor_add. 
  replace (seqfor
  (fun i : fin n => f (exist (fun i0 : nat => i0 < S m) m (Nat.lt_succ_diag_r m)) (fin2finS i))
  (seqfor (fun i : fin (m * S n) => f (fin2finS (nat2fin m (i / S n))) (nat2fin (S n) (i mod S n)))
     x)) with (((seqfor (fun i : fin (m * S n) => f (fin2finS (nat2fin m (i / S n))) (nat2fin (S n) (i mod S n))))'; seqfor
  (fun i : fin n => f (exist (fun i0 : nat => i0 < S m) m (Nat.lt_succ_diag_r m)) (fin2finS i))) x).
  f_equal. - induction m;auto. f_equal. fun_ext. 
  f_equal. autorewrite with core. apply fin_eq. autorewrite with core. auto.
  apply Nat.div_lt_upper_bound. auto. rewrite Nat.mul_comm. induction x0;simpl. lia.
  apply Nat.div_lt_upper_bound. auto. rewrite Nat.mul_comm. induction x0;simpl. lia.
  induction x0;simpl. lia. apply fin_eq. autorewrite with core. auto. induction x0;auto.
  simpl. lia. autorewrite with core. apply Nat.mod_upper_bound. auto. induction x0;simpl; lia.
  apply Nat.mod_upper_bound;auto.
  - induction n;auto. f_equal. fun_ext. f_equal. 
  replace (fin2finS (nat2fin (S n + m * S (S n)) (x0 + m * S (S n))) / S (S n)) with m. unfold nat2fin.
  destruct (le_lt_dec (S m) m). lia. f_equal. apply lt_unique.
  autorewrite with core. rewrite Nat.div_add,Nat.div_small;auto.
  assert (x0 < S n);auto. lia. apply fin_eq. autorewrite with core. rewrite Nat.mod_add,Nat.mod_small;auto.
  induction x0;simpl;lia. autorewrite with core. rewrite Nat.mod_add,Nat.mod_small;auto. induction x0; simpl; lia.
  - unfold seq;auto.
Qed.

Fixpoint parfor {d:data}{m:nat}:(fin m -> acc d -> comm) -> acc (ary '{m} d) -> comm :=
  match m with
  | O => fun (p: fin O -> acc d -> comm ) _ => skip
  | S m' => fun (p: fin (S m') -> acc d -> comm ) v
         => parfor (fun i => p (fin2finS i)) (fst v) ';
            p (exist _ m' (Nat.lt_succ_diag_r m')) (snd v)
  end.

Lemma parfor_Sn: forall d m p (a:acc (ary '{ S m} d)),
  parfor p a
  = parfor (fun i => p (fin2finS i)) (fst a) ';
    p (exist _ m (Nat.lt_succ_diag_r m)) (snd a).
Proof. auto. Qed.

Hint Rewrite seqfor_Sn parfor_Sn mk_vec_Sn.

Fixpoint for_rev (n:nat) :(fin n -> comm)->comm:=
  match n with
  | O => fun (p: fin O -> comm) => skip
  | S n' => fun (p: fin (S n') -> comm)
      =>p (exist _ n' (Nat.lt_succ_diag_r n')) '; 
        for_rev n' (fun i => p (fin2finS i)) 
  end.

Lemma for_rev_Sn: forall (m:nat)(p: fin (S m) -> comm),
  for_rev (S m) p = 
  p (exist _ m (Nat.lt_succ_diag_r m)) '; 
  for_rev m (fun i => p (fin2finS i)) .
Proof. auto. Qed.

Hint Rewrite for_rev_Sn.

Fixpoint vrd {d:data}(eta:env): acc d -> exp d:=
  match d with
  | num => fun (p:acc num) => eta p
  | @ary n m d1 => fun p => mk_vec (fun (i:fin m) =>
      vrd eta p|{i})
  | tensor d1 => fun (p:acc (tensor d1)) =>
      (vrd eta (pairAcc1 p),
       vrd eta (pairAcc2 p))
  end. 

Fixpoint assign {d:data} : acc d -> exp d -> comm :=
  match d with
  | num => fun (a:acc num) (e: exp num) (eta:env) => update eta a e
  | @ary n m d1 => fun a (e: exp (@ary n m d1)) =>
    seqfor (fun i =>(assign a|{i} e|[i]) )
  | tensor d1 =>  fun a (e: exp (tensor d1)) =>
    assign (pairAcc1 a)(fst e) ';
    assign (pairAcc2 a)(snd e)
end.

Fixpoint vrm {d:data} : acc d -> comm :=
  match d with
  | num => fun(a:acc num) (eta:env) => remove a eta
  | @ary n m d1 => fun a => 
    for_rev m (fun i  => (vrm a|{i}) )
  | tensor d1 => fun a => vrm (pairAcc2 a) ';vrm (pairAcc1 a)
  end.

Definition new {d:data} (p: acc d -> comm) (a:acc d) : comm := 
  p a '; vrm a.

Hint Unfold seq new.

Notation " p1 '; p2 " := (seq p1 p2) (at level 65,right associativity).
Notation " a |:= e " := (assign a e ) (at level 60).

Local Open Scope R_scope.

Section ProofofAuxiliaryLemma.

Lemma assign_vrd: forall d (a:path) eta,
  ((@acc' d a) |:= (vrd eta (acc' a))) eta = eta.
Proof.
  induction d. - simpl. intros. apply update_same.
  - simpl. autounfold. induction f;simpl.
    induction x;auto. intros. autorewrite with core. 
    rewrite ?v_nth_x. unfold seq. induction x;auto.
    replace (fun i : fin (S x) =>@assign d (@v_nth (acc d) (S (S x)) (acc_default d)
      (@pair (vector (acc d) (S x)) (acc d) (@mk_vec (acc d) (S x)
      (fun i0 : fin (S x) => @acc' d (AryIdx n (nat2fin n (@fin2nat (S (S x)) (@fin2finS (S x) i0))) a))) 
      (@acc' d (AryIdx n (nat2fin n (S x)) a))) (@fin2nat (S (S x)) (@fin2finS (S x) i)))
      (@v_nth (exp d) (S (S x)) (exp_default d) (@pair (vector (exp d) (S x)) (exp d)
      (@mk_vec (exp d) (S x) (fun i0 : fin (S x) => @vrd d eta (@v_nth (acc d) (S (S x)) 
      (acc_default d) (@pair (vector (acc d) (S x)) (acc d) (@mk_vec (acc d) (S x)
      (fun i1 : fin (S x) => @acc' d (AryIdx n (nat2fin n (@fin2nat (S (S x)) (@fin2finS (S x) i1))) a)))
      (@acc' d (AryIdx n (nat2fin n (S x)) a))) (@fin2nat (S (S x)) (@fin2finS (S x) i0)))))
      (@vrd d eta (@acc' d (AryIdx n (nat2fin n (S x)) a)))) (@fin2nat (S (S x)) (@fin2finS (S x) i)))) with
      (fun i : fin (S x) => v_nth (acc_default d) (mk_vec (fun i0 : fin (S x) => acc' (AryIdx n (nat2fin n i0) a))) i
      |:= v_nth (exp_default d) (mk_vec (fun i0 : fin (S x) => vrd eta (v_nth (acc_default d)(mk_vec 
      (fun i1 : fin (S x) => acc' (AryIdx n (nat2fin n i1) a))) i0))) i).
    rewrite IHx. apply IHd. lia. fun_ext. f_equal;repeat f_equal.
    rewrite v_nth_Sn;auto. induction x0;auto.
    rewrite v_nth_Sn;auto. repeat f_equal. fun_ext.
    rewrite v_nth_Sn;induction x1,x0;auto. induction x0;auto.
    - simpl. unfold seq. intros. rewrite ?IHd. auto.
Qed.

Lemma vrd_assign_aux: forall n d (a1 a2:path) x (e: vector (exp d) (S x))  x0 eta,
  a1 =? a2 = false ->
  (forall (a1 a2 : path) (e : exp d) (eta : env),
    vrd ((acc' a1 |:= e) eta) (acc' a2) =
    (if a1 =? a2 then e else vrd eta (acc' a2))) ->
  vrd (seqfor (fun i0 : fin x => v_nth (acc_default d) (mk_vec
    (fun i1 : fin x =>acc' (AryIdx n (nat2fin n i1) a1))) i0
    |:= v_nth (exp_default d) e i0) eta) (acc' (AryIdx n (nat2fin n x0) a2)) =
  vrd eta (@acc' d (AryIdx n (nat2fin n x0) a2)).
Proof.
  induction x,e;auto.
  intros. autorewrite with core. unfold seq. rewrite ?v_nth_x.
  rewrite H0. replace (AryIdx n (nat2fin n x) a1 =? AryIdx n (nat2fin n x0) a2) with false.
  induction x;auto.
  replace (fun i : fin (S x) => @assign d (@v_nth (acc d) (S (S x)) (acc_default d)
    (@pair (vector (acc d) (S x)) (acc d) (@mk_vec (acc d) (S x)
    (fun i0 : fin (S x) => @acc' d (AryIdx n (nat2fin n (@fin2nat (S (S x))
    (@fin2finS (S x) i0))) a1))) (@acc' d (AryIdx n (nat2fin n (S x)) a1)))
    (@fin2nat (S (S x)) (@fin2finS (S x) i))) (@v_nth (exp d) (S (S (S x))) (exp_default d)
    (@pair (vector (exp d) (S (S x))) (exp d) v e) (@fin2nat (S (S x)) (@fin2finS (S x) i))))
  with (fun i0 : fin (S x) => v_nth (acc_default d) (mk_vec (fun i1 : fin (S x) =>
    acc' (AryIdx n (nat2fin n i1) a1))) i0|:= v_nth (exp_default d) v i0).
  apply IHx;auto. fun_ext. rewrite v_nth_Sn.
  f_equal. rewrite v_nth_Sn. f_equal. auto. induction x1;auto.
  simpl. rewrite H,?Bool.andb_false_r. auto.
Qed.

Lemma vrd_assign: forall d (a1:path) (a2:path) (e:exp d) eta,
  vrd (((acc' a1)|:= e) eta) (acc' a2) = if a1 =? a2 then e else vrd eta (acc' a2).
Proof.
  induction d. 
  - intros. destruct (a1 =? a2) eqn:E.
    * apply path_eqb_eq in E;subst. simpl. apply update_eq.
    * apply path_eqb_neq in E. simpl. apply update_neq;auto.
  - simpl. unfold idx,idxAcc. induction f;simpl. intros.
    destruct (a1 =? a2) eqn:E.
    * autounfold. induction x,e;auto. rewrite mk_vec_Sn;auto.
      f_equal. rewrite <- IHx;try lia. induction x;auto.
      f_equal. fun_ext. rewrite v_nth_mk_vec. rewrite seqfor_Sn.
      unfold seq. rewrite v_nth_mk_vec. rewrite IHd.
      replace (path_eqb (AryIdx n (nat2fin n (@fin2nat (S (S x))
        (nat2fin (S (S x)) (@fin2nat (S (S x)) 
        (@exist nat (fun i : nat => lt i (S (S x))) 
        (S x) (Nat.lt_succ_diag_r (S x))))))) a1)
        (AryIdx n (nat2fin n (@fin2nat (S (S x)) (nat2fin (S (S x))
        (@fin2nat (S (S x)) (@fin2finS (S x) x0))))) a2)) with false.
      repeat f_equal. fun_ext. rewrite mk_vec_Sn.
      rewrite v_nth_Sn;auto. repeat f_equal. rewrite v_nth_Sn;auto.
      induction x1;auto. induction x1;auto. rewrite v_nth_mk_vec. repeat f_equal.
      autorewrite with core;auto. auto. autorewrite with core.
      induction x0;simpl. rewrite Nat.eqb_refl,E. simpl.
      replace (nat2fin n (S x) =? nat2fin n x0)%nat with false. auto.
      autorewrite with core. symmetry. apply Nat.eqb_neq. lia. lia. lia. induction x0;auto.
      lia. simpl. lia. induction x0;auto. rewrite v_nth_mk_vec.
      rewrite seqfor_Sn. unfold seq. rewrite v_nth_mk_vec.
      autorewrite with core. rewrite IHd.
      apply path_eqb_eq in E;subst. rewrite path_eqb_refl.
      apply v_nth_x. auto. auto. auto.
    * autounfold. induction x;auto. autorewrite with core. unfold seq.
      f_equal. induction x;auto. f_equal. fun_ext. rewrite v_nth_x;auto.
      rewrite v_nth_Sn;auto. replace (@fin2nat (S (S x)) (@fin2finS (S x) x0)) with
      (@fin2nat (S x) x0). rewrite ?v_nth_mk_vec.
      rewrite IHd. replace (AryIdx n (nat2fin n (S x)) a1 =?
      AryIdx n (nat2fin n (fin2finS (nat2fin (S x) x0))) a2) with
      false. rewrite ?nat2fin_fin2finS. 
      replace (fun i : fin (S x) => @assign d (@v_nth (acc d) (S (S x)) (acc_default d)
        (@pair (vector (acc d) (S x)) (acc d) (@mk_vec (acc d) (S x)
        (fun i0 : fin (S x) => @acc' d (AryIdx n (nat2fin n (@fin2nat (S (S x))
        (@fin2finS (S x) i0))) a1)))(@acc' d (AryIdx n (nat2fin n (S x)) a1)))
        (@fin2nat (S (S x)) (@fin2finS (S x) i))) (@v_nth (exp d) (S (S x)) (exp_default d) e
        (@fin2nat (S (S x)) (@fin2finS (S x) i))))
      with (fun i0 : fin (S x) => v_nth (acc_default d) (mk_vec (fun i1 : fin (S x) =>
        acc' (AryIdx n (nat2fin n i1) a1))) i0 |:= v_nth (exp_default d) e i0).
      replace (nat2fin (S x) x0) with x0.
      apply vrd_assign_aux;auto. apply fin_eq.
      induction x0;auto. autorewrite with core;auto. 
      fun_ext. rewrite v_nth_Sn. f_equal. induction x1;auto.
      lia. simpl. rewrite E,?Bool.andb_false_r. auto. auto.
      induction x0;auto. induction x0;auto. rewrite ?v_nth_x. rewrite IHd.
      replace (AryIdx n (nat2fin n x) a1 =? AryIdx n (nat2fin n x) a2) with false.
      induction x;auto.      
      replace (fun i : fin (S x) => @assign d (@v_nth (acc d) (S (S x)) (acc_default d)
        (@pair (vector (acc d) (S x)) (acc d) (@mk_vec (acc d) (S x)
        (fun i0 : fin (S x) => @acc' d (AryIdx n (nat2fin n
        (@fin2nat (S (S x)) (@fin2finS (S x) i0))) a1))) (@acc' d (AryIdx n (nat2fin n (S x)) a1)))
        (@fin2nat (S (S x)) (@fin2finS (S x) i))) (@v_nth (exp d) (S (S x)) (exp_default d) e
        (@fin2nat (S (S x)) (@fin2finS (S x) i))))
      with (fun i0 : fin (S x) => v_nth (acc_default d)
        (mk_vec (fun i1 : fin (S x) => acc' (AryIdx n (nat2fin n i1) a1))) i0
        |:= v_nth (exp_default d) e i0).
       apply vrd_assign_aux;auto. fun_ext.
      rewrite v_nth_Sn. f_equal. induction x0;auto.
      simpl. rewrite E,?Bool.andb_false_r. auto.
    - simpl. intros. unfold seq;simpl. induction e. destruct (a1=?a2) eqn:E.
      apply path_eqb_eq in E;subst.
      rewrite IHd. replace (PairR a2 =? PairL a2) with false.
      f_equal;rewrite IHd,path_eqb_refl; auto. auto.
      rewrite ?IHd. replace (PairR a1 =? PairL a2) with false.
      replace (PairL a1 =? PairL a2) with false. f_equal.
      replace (PairR a1 =? PairR a2) with false. 
      replace (PairL a1 =? PairR a2) with false. auto.
      auto. auto.
Qed.

Lemma vrm_assign: forall d (a:path) (e:exp d) eta,
  @vrm d (acc' a) ((acc' a |:= e) eta) = eta.
Proof.
  induction d. - simpl. intros. apply remove_update.
  - simpl. autounfold. induction f. simpl. induction x,e;auto.
    intros. autorewrite with core. unfold seq. rewrite ?v_nth_x.
    rewrite IHd. induction x;auto. rewrite <-IHx with (a:=a)(e:=v).
    f_equal. fun_ext. rewrite ?v_nth_Sn;auto. replace (fin2nat (fin2finS x0)) with (fin2nat x0).
    rewrite ?v_nth_mk_vec. f_equal;auto. induction x0;auto. f_equal.
    fun_ext. rewrite ?v_nth_Sn;auto. induction x0;auto.
    induction x0;auto. lia.
  - induction e. intros. simpl. unfold seq.
    rewrite ?IHd. auto.
Qed.

Lemma assign_assign_aux:forall n x d a1 a2 (f:nat->exp d) e2 eta, 
  (forall (i:fin x), AryIdx n (nat2fin n i) a1 =? a2 = false) ->
  (forall (a1 a2 : path) (e1 e2 : exp d) (eta : env),
      (acc' a1 |:= e1) ((acc' a2 |:= e2) eta) =
      (if a1 =? a2 then (acc' a1 |:= e1) eta
       else (acc' a2 |:= e2) ((acc' a1 |:= e1) eta))) ->
  seqfor (fun i : fin x => @v_nth (acc d) x (acc_default d)
    (mk_vec (fun i0 : fin x => acc' (AryIdx n (nat2fin n i0) a1))) i|:= f i) ((acc' a2|:= e2) eta)
  = (@acc' d a2|:= e2) (seqfor (fun i : fin x => v_nth (acc_default d)
    (mk_vec (fun i0 : fin x => acc' (AryIdx n (nat2fin n i0) a1)))i |:= f i ) eta).
Proof.
  induction x;auto.
  intros. autorewrite with core. unfold seq.
  rewrite ?v_nth_x. rewrite H0.
  replace (a2 =? AryIdx n (nat2fin n x) a1) with false.
  f_equal. induction x;auto. 
  replace (fun i : fin (S x) => @v_nth (acc d) (S (S x))(acc_default d)
    (mk_vec (fun i0 : fin (S x) => acc' (AryIdx n (nat2fin n (fin2finS i0)) a1)),
    acc' (AryIdx n (nat2fin n (S x)) a1)) (fin2finS i)|:= f (fin2finS i)) 
  with (fun i : fin (S x) => v_nth (acc_default d) (mk_vec 
    (fun i0 : fin (S x) => acc' (AryIdx n (nat2fin n i0) a1))) i |:= f i).
  rewrite IHx;auto. intros. replace (nat2fin n i) with (nat2fin n (fin2finS i)).
  auto. induction i. simpl. auto. fun_ext. rewrite v_nth_Sn. f_equal. induction x0;auto.
  symmetry. apply path_eqb_sym. replace x with (fin2nat (nat2fin (S x) x)). auto. auto.
Qed.

Lemma assign_assign: forall d (a1 a2:path) (e1 e2:exp d) eta,
  @assign d (acc' a1) e1 (assign (acc' a2) e2 eta) = 
  if path_eqb a1 a2 then assign (acc' a1) e1 eta else @assign d (acc' a2) e2 (assign (acc' a1) e1 eta).
Proof.
  induction d.
  - intros. destruct (a1 =? a2) eqn:E.
    * apply path_eqb_eq in E;subst. simpl. apply update_shadow.
    * apply path_eqb_neq in E. simpl. apply update_permute;auto.
  - intros. destruct (a1 =? a2) eqn:E.
    * simpl. autounfold. apply path_eqb_eq in E;subst. autounfold. induction f;simpl.
      induction x,e1,e2;auto. autorewrite with core. unfold seq.
      rewrite ?v_nth_x. induction x. simpl. unfold skip. rewrite IHd.
      rewrite path_eqb_refl. auto.
      replace (fun i : fin (S x) => @v_nth (acc d) (S (S x)) (acc_default d)
        (mk_vec (fun i0 : fin (S x) => acc' (AryIdx n (nat2fin n (fin2finS i0)) a2)),
        acc' (AryIdx n (nat2fin n (S x)) a2)) (fin2finS i)
        |:= @v_nth (exp d) (S (S x)) (exp_default d) (v, e) (fin2finS i)) 
      with (fun i : fin (S x) => @v_nth (acc d) (S x) (acc_default d)
        (mk_vec (fun i0 : fin (S x) => acc' (AryIdx n (nat2fin n i0) a2))) i
        |:= v_nth (exp_default d) v i).
    rewrite assign_assign_aux;auto. rewrite IHd,path_eqb_refl. f_equal.
    assert (H:(S x <= n)%nat). lia.
    replace (fun i : fin (S x) => @v_nth (acc d) (S (S x)) (acc_default d)
      (mk_vec (fun i0 : fin (S x) => acc' (AryIdx n (nat2fin n (fin2finS i0)) a2)),
      acc' (AryIdx n (nat2fin n (S x)) a2)) (fin2finS i)
      |:= @v_nth (exp d) (S (S x)) (exp_default d) (v0, e0) (fin2finS i)) 
    with (fun i : fin (S x) => v_nth (acc_default d) (mk_vec
      (fun i0 : fin (S x) => acc' (AryIdx n (nat2fin n i0) a2))) i
      |:= v_nth (exp_default d) v0 i).
    replace (fun i : fin (S x) => v_nth (acc_default d) (mk_vec
      (fun i0 : fin (S x) => acc' (AryIdx n (nat2fin n (fin2finS i0)) a2))) 
      (fin2finS i) |:= v_nth (exp_default d) v (fin2finS i)) 
    with (fun i : fin (S x) => v_nth (acc_default d) (mk_vec
      (fun i0 : fin (S x) => acc' (AryIdx n (nat2fin n i0) a2)))
      i |:= v_nth (exp_default d) v i).
    rewrite(IHx H v v0). repeat f_equal. fun_ext.
    repeat f_equal. fun_ext. repeat f_equal. rewrite ?v_nth_Sn;auto.
    repeat f_equal. induction x0;auto. rewrite v_nth_Sn;auto.
    induction x0;auto. induction i;simpl. rewrite Nat.eqb_refl,path_eqb_refl,?fin2nat_nat2fin;auto.
    simpl. rewrite Bool.andb_true_r. apply Nat.eqb_neq. lia. lia.
    fun_ext. rewrite v_nth_Sn. repeat f_equal. rewrite v_nth_Sn;auto.
    induction x0;auto. induction x0;auto.
    * simpl. autounfold. induction f. simpl.
      induction x,e1,e2;auto. autorewrite with core. unfold seq.
      rewrite ?v_nth_x. induction x. simpl. unfold skip. rewrite IHd. 
      replace (AryIdx n (nat2fin n 0) a1 =? AryIdx n (nat2fin n 0) a2) with false. auto.
      simpl. rewrite E,?Bool.andb_false_r. auto.
      replace (fun i : fin (S x) => @v_nth (acc d) (S (S x)) (acc_default d)
        (mk_vec (fun i0 : fin (S x) => acc' (AryIdx n (nat2fin n (fin2finS i0)) a1)),
        acc' (AryIdx n (nat2fin n (S x)) a1)) (fin2finS i)
        |:= @v_nth (exp d) (S (S x)) (exp_default d) (v, e) (fin2finS i)) 
      with (fun i : fin (S x) => @v_nth (acc d) (S x) (acc_default d)
        (mk_vec (fun i0 : fin (S x) => acc' (AryIdx n (nat2fin n i0) a1)))i
        |:= v_nth (exp_default d) v i).
      replace (fun i : fin (S x) => @v_nth (acc d) (S (S x)) (acc_default d)
        (mk_vec (fun i0 : fin (S x) => acc' (AryIdx n (nat2fin n (fin2finS i0)) a2)),
        acc' (AryIdx n (nat2fin n (S x)) a2)) (fin2finS i)
        |:= @v_nth (exp d) (S (S x)) (exp_default d) (v0, e0) (fin2finS i)) 
      with (fun i : fin (S x) => v_nth (acc_default d) (mk_vec
        (fun i0 : fin (S x) => acc' (AryIdx n (nat2fin n i0) a2))) i
        |:= v_nth (exp_default d) v0 i).
   rewrite ?assign_assign_aux;auto. rewrite IHd.
   replace (AryIdx n (nat2fin n (S x)) a1 =?
   AryIdx n (nat2fin n (S x)) a2) with false.
   rewrite IHx. auto. lia. simpl. rewrite E,?Bool.andb_false_r;auto.
   simpl. apply path_eqb_sym in E;rewrite E. intros.
   rewrite ?Bool.andb_false_r;auto. simpl. intros.
   rewrite E,?Bool.andb_false_r;auto. fun_ext.
   rewrite v_nth_Sn. f_equal. rewrite v_nth_Sn;auto. induction x0;auto.  induction x0;auto.
   fun_ext. rewrite v_nth_Sn. f_equal. rewrite v_nth_Sn;auto. induction x0;auto.  induction x0;auto.
    - intros. destruct (a1=?a2) eqn:E. induction e1,e2. apply path_eqb_eq in E;subst.
    simpl. unfold seq. rewrite (IHd (PairL a2) (PairR a2)).
    replace (PairL a2 =? PairR a2) with false.
    rewrite IHd. replace (PairR a2 =? PairR a2) with true.
    f_equal. rewrite IHd. replace (PairL a2 =? PairL a2) with true.
    auto. simpl. rewrite path_eqb_refl. auto. simpl. rewrite path_eqb_refl;auto. auto.
    induction e1,e2. simpl. unfold seq. rewrite (IHd (PairL a1)(PairR a2)).
    replace (PairL a1 =? PairR a2) with false;auto.
    rewrite (IHd (PairR a1) (PairR a2)).
    replace (PairR a1 =? PairR a2) with false;auto.
    f_equal. rewrite (IHd (PairL a2)(PairR a1)). 
    replace (PairL a2 =? PairR a1) with false;auto.
    f_equal. rewrite IHd.
    replace (PairL a1 =? PairL a2) with false;auto.
Qed.

Lemma assign_assign1: forall d (a1 a2:path) (e1 e2:exp d),
  @acc' d a2 |:= e2 '; @acc' d a1 |:= e1  = 
  if path_eqb a1 a2 then @acc' d a1 |:= e1 else @acc' d a1 |:= e1 '; @acc' d a2 |:= e2 .
Proof.
  intros. destruct (a1 =? a2) eqn:E;unfold seq;fun_ext; rewrite assign_assign,E;auto.
Qed.

End ProofofAuxiliaryLemma.

Lemma new_equiv: forall d (c: exp d -> comm) (e1:exp d)(a:path)  ,
  (forall e e1 x, c e1 (((acc' a) |:= e) x) = ((@acc' d a)|:= e) (c e1 x)) ->
  @new d (fun a0 => a0 |:= e1 '; (fun eta => c (vrd eta a0) eta)) (acc' a) = c e1 .
Proof.
  unfold new,seq,assign. intros. fun_ext.
  rewrite vrd_assign. rewrite path_eqb_refl. rewrite H. rewrite vrm_assign. auto.
Qed.

Lemma reducel_equiv_aux: forall n d1 d2 (f:exp d1-> exp d2 -> exp d2) i (e:vector (exp d1) n) a1 eta,
  (acc' a1 |:= v_reduce f i e) eta  =
  seqfor (fun (i0 : fin n) (eta : env) =>
    (acc' a1 |:= f (v_nth (exp_default d1) e i0) (vrd eta (acc' a1))) eta) ((acc' a1 |:= i) eta).
Proof.
  induction n,e;auto.
  intros. autorewrite with core. unfold seq.
  simpl v_reduce. induction n. simpl. unfold skip.
  rewrite assign_assign,path_eqb_refl.
  rewrite vrd_assign,path_eqb_refl. auto.
  replace (fun (i0 : fin (S n)) (eta0 : env) => @assign d2 (@acc' d2 a1)
    (f (@v_nth (exp d1) (S (S n)) (exp_default d1) (@pair (vector (exp d1) (S n)) (exp d1) v e)
    (@fin2nat (S (S n)) (@fin2finS (S n) i0))) (@vrd d2 eta0 (@acc' d2 a1))) eta0) 
  with (fun (i0 : fin (S n)) (eta0 : env) => (acc' a1
    |:= f (v_nth (exp_default d1) v i0) (vrd eta0 (acc' a1)))eta0).
  rewrite <- IHn. rewrite assign_assign,vrd_assign,path_eqb_refl.
  rewrite v_nth_x.  auto. repeat fun_ext. repeat f_equal.
  rewrite v_nth_Sn. f_equal. induction x;auto.
Qed.

Lemma reducel_equiv: forall n d1 d2 (f:exp d1 -> exp d2 -> exp d2) (i:exp d2) (a a1:path) (e:exp (ary '{n} d1)) , a<>a1 ->
  (acc' a) |:= reduce f i e =
    @new d2 (fun a0 => 
      a0 |:= i '; @seqfor n (fun (i0: fin n) eta => (a0 |:= f e |[ i0] (vrd eta a0)) eta) ';
        fun eta => ((acc' a) |:= (vrd eta a0)) eta) (acc' a1).
Proof.
  autounfold. intros. fun_ext. rewrite <- reducel_equiv_aux.
  rewrite vrd_assign,path_eqb_refl. rewrite assign_assign. apply path_eqb_neq in H. rewrite H.
  rewrite vrm_assign. auto.
Qed.

Lemma assign_ary_par: forall m (n : fle m) (d : data) (a : path) (x : exp (ary n d)),
  acc' a |:= x =
  parfor (fun (i: fin n) (o : acc d) => o |:= x |[i]) (@acc' (ary n d) a).
Proof.
  intros. fun_ext.
  simpl. autounfold. induction n;auto. unfold idx,idxAcc. intros. simpl. 
  induction x1,x;auto. autorewrite with core. unfold seq. f_equal.
  rewrite v_nth_x. unfold snd. auto. unfold fst.
  induction x1;auto.
  replace (fun i : fin (S x1) => @v_nth (acc d) (S (S x1)) (acc_default d)
    (mk_vec (fun i0 : fin (S x1) => acc' (AryIdx m (nat2fin m (fin2finS i0)) a)),
    acc' (AryIdx m (nat2fin m (S x1)) a)) (fin2finS i) |:= @v_nth (exp d) (S (S x1)) (exp_default d) (v, e) (fin2finS i))
  with (fun i : fin (S x1) => v_nth (acc_default d)
    (mk_vec (fun i0 : fin (S x1) => acc' (AryIdx m (nat2fin m i0) a))) i
    |:= v_nth (exp_default d) v i).
  rewrite IHx1. f_equal. repeat fun_ext. f_equal. rewrite v_nth_Sn;auto.
  induction x;auto. lia. fun_ext. repeat f_equal.
  rewrite v_nth_Sn. f_equal. induction x;auto. rewrite v_nth_Sn. f_equal.
  induction x;auto.
Qed.

Lemma assign_tensor: forall (d : data) (a : path) (x : exp (tensor d)), 
  (acc' a) |:= x = pairAcc1 (acc' a) |:= Fst x '; pairAcc2 (acc' a) |:= Snd x.
Proof. auto. Qed.

Lemma assign_pair: forall (d : data) (e1 e2 : exp d) (a : path),
  acc' a |:= Pair e1 e2 = pairAcc1 (acc' a) |:= e1 '; pairAcc2 (acc' a) |:= e2.
Proof. auto. Qed.

Lemma mapSeq_equiv : forall m (n : fle m) (d1 d2 : data) (f : exp d1 -> exp d2) (v:exp (ary n d1)) (a :path),
  @acc' (ary n d2)  a |:= mapSeq f v  = seqfor (fun i : fin n => (@acc' (ary n d2)  a)|{i} |:= f v|[i]).
Proof. induction n. simpl. autounfold. unfold v_map,v_idx.
  induction x;auto. intros. f_equal. fun_ext.
  repeat f_equal. rewrite v_nth_mk_vec;autorewrite with core;induction x0;auto.
Qed.

Lemma mapPar_equiv : forall m (n : fle m) (d1 d2 : data) (f : exp d1 -> exp d2) (v:exp (ary n d1)) (a : path),
  @acc' (ary n d2) a |:= mapPar f v  = parfor (fun (i : fin n) o => o |:= f v|[i]) (@acc' (ary n d2) a ).
Proof.  intros.  rewrite assign_ary_par. induction n. simpl.
  unfold idxAcc,idx,mapPar,v_map,v_idx.
  induction x;auto. intros. f_equal. repeat fun_ext.
  repeat f_equal. rewrite v_nth_mk_vec;autorewrite with core;
  induction x0;auto.
Qed.

Lemma zip_equiv_aux: forall d m x (a a1:path) (f:nat -> exp d) e eta,
  (forall i : fin x,(PairR(AryIdx m (nat2fin m i) a) =? a1) = false) ->
  seqfor(fun i : fin x => v_nth (acc_default d) (mk_vec
    (fun i0 : fin x => acc' (PairR (AryIdx m (nat2fin m i0) a)))) i |:= f i)
    ((acc' a1|:= e) eta) 
  = (@acc' d a1|:= e) (seqfor (fun i : fin x => v_nth (acc_default d)
    (mk_vec (fun i0 : fin x => acc' (PairR (AryIdx m (nat2fin m i0) a)))) i |:= f i) eta).
Proof.
  induction x;auto. intros. autorewrite with core. 
  unfold seq. rewrite ?v_nth_x. rewrite assign_assign.
  replace (a1 =? PairR (AryIdx m (nat2fin m x) a)) with false.
  f_equal. induction x;auto.
  replace (fun i : fin (S x) => @v_nth (acc d) (S (S x))(acc_default d)
    (mk_vec (fun i0 : fin (S x) => acc' (PairR (AryIdx m (nat2fin m (fin2finS i0)) a))),
    acc' (PairR (AryIdx m (nat2fin m (S x)) a))) (fin2finS i) |:= f (fin2finS i))
  with (fun i : fin (S x) => v_nth (acc_default d) (mk_vec
    (fun i0 : fin (S x) =>acc' (PairR (AryIdx m (nat2fin m i0) a)))) i |:= f i).
  rewrite IHx;auto. intros. replace (fin2nat i) with (fin2nat (fin2finS i)).
  auto. induction i;auto. fun_ext. rewrite v_nth_Sn.
  f_equal. induction x0;auto. symmetry. apply path_eqb_sym.
  replace x with (fin2nat(nat2fin (S x) x));auto.
Qed.

Lemma fst_aux: forall A B (x:A) (y:B) ,
  fst (x,y) = x.
Proof. auto. Qed.

Lemma snd_aux: forall A B (x:A) (y:B) ,
  snd (x,y) = y.
Proof. auto. Qed.

Lemma zip_equiv : forall m (n:fle m) d (a: path) (e1 e2:exp(ary n d)), 
  @acc' (ary n (tensor d)) a |:= zip e1 e2 
  = zipAcc1 (@acc' (ary n (tensor d)) a) |:= e1 '; zipAcc2 (@acc' (ary n (tensor d)) a) |:= e2.
Proof. 
  intros. simpl.
  unfold zipAcc1,zipAcc2,zip,pairAcc1,pairAcc2,idxAcc,idx,seq,v_zip,v_idx.
  induction n;simpl. fun_ext. induction x;auto.
  rewrite ?seqfor_Sn with (m:= x);unfold seq. f_equal.
  rewrite v_nth_mk_vec. unfold snd. rewrite v_unzip2_mk_vec.
  rewrite v_nth_mk_vec;auto. rewrite fin2nat_exist;auto.
  rewrite v_nth_mk_vec;auto. unfold snd.
  f_equal. autorewrite with core;auto. rewrite ?v_nth_mk_vec;auto.
  rewrite v_unzip1_mk_vec,v_unzip2_mk_vec.
  rewrite v_nth_mk_vec;auto. rewrite ?fst_aux,?snd_aux.
  autorewrite with core;auto. induction x;auto.
  replace (fun i : fin (S x) => @assign d (@v_nth (acc d) (S (S x)) (acc_default d)
    (@pair (vector (acc d) (S x)) (acc d) (@mk_vec (acc d) (S x)
    (fun i0 : fin (S x) => @acc' d
    (PairR (AryIdx m (nat2fin m (@fin2nat (S (S x)) (@fin2finS (S x) i0))) a))))
    (@acc' d (PairR (AryIdx m (nat2fin m (S x)) a))))(@fin2nat (S (S x)) (@fin2finS (S x) i)))
    (@v_nth (exp d) (S (S x)) (exp_default d) e2 (@fin2nat (S (S x)) (@fin2finS (S x) i))))
  with (fun i : fin (S x) => v_nth (acc_default d) (mk_vec (fun i0 : fin (S x) =>
    acc' (PairR (AryIdx m (nat2fin m i0) a)))) i |:= v_nth (exp_default d) e2 i).
  rewrite zip_equiv_aux. f_equal. induction e1,e2.
  replace (fun i : fin (S x) => @assign d (@v_nth (acc d) (S x) (acc_default d)
    (@mk_vec (acc d) (S x) (fun i0 : fin (S x) => @acc' d
    (PairR (AryIdx m (nat2fin m (@fin2nat (S x) i0)) a))))
    (@fin2nat (S x) i)) (@v_nth (exp d) (@fle2nat m
    (@exist nat (fun i0 : nat => le i0 m) (S (S x)) p))
    (exp_default d) (@pair (vector (exp d) (S x)) (exp d) v e)
    (@fin2nat (S x) i)))
  with (fun i : fin (S x) => v_nth (acc_default d)
    (v_unzip2 (acc_default d, acc_default d) (mk_vec
    (fun i0 : fin (S x) => (acc' (PairL (AryIdx m (nat2fin m i0) a)),
    acc' (PairR (AryIdx m (nat2fin m i0) a)))))) i |:= v_nth (exp_default d) v i).
  replace (fun i : fin (S x) => @assign d (@v_nth (acc d) (S (S x)) (acc_default d)
    (@pair (vector (acc d) (S x)) (acc d) (@mk_vec (acc d) (S x)
    (fun i0 : fin (S x) => @acc' d (PairL (AryIdx m (nat2fin m
    (@fin2nat (S (S x))(@fin2finS (S x) i0))) a)))) (@acc' d (PairL (AryIdx m (nat2fin m (S x)) a))))
    (@fin2nat (S (S x)) (@fin2finS (S x) i))) (@v_nth (exp d) (S (S x)) (exp_default d) 
    (@pair (vector (exp d) (S x)) (exp d) a0 b) (@fin2nat (S (S x)) (@fin2finS (S x) i)))) 
  with (fun i : fin (S x) => v_nth (acc_default d) (v_unzip1 (acc_default d, acc_default d)
    (mk_vec (fun i0 : fin (S x) => (acc' (PairL (AryIdx m (nat2fin m i0) a)),
    acc' (PairR (AryIdx m (nat2fin m i0) a)))))) i |:= v_nth (exp_default d) a0 i).
    rewrite <-IHx. repeat f_equal. repeat fun_ext.
    repeat f_equal. rewrite v_nth_Sn. f_equal.
    induction x1;auto. rewrite v_nth_Sn. repeat f_equal.
    fun_ext. rewrite ?v_nth_Sn;induction x4;auto. induction x1;auto.
    rewrite v_nth_Sn. f_equal. induction x1;auto.
    rewrite v_nth_Sn. repeat f_equal. fun_ext. rewrite ?v_nth_Sn;induction x4;auto.
    induction x1;auto. lia. fun_ext. rewrite v_unzip1_mk_vec. rewrite v_nth_Sn. f_equal.
    rewrite v_nth_Sn;auto. induction x1;auto. induction x1;auto.
    fun_ext. rewrite v_unzip2_mk_vec. f_equal.
    rewrite <- v_nth_Sn with(b:=e). auto. induction x1;auto.
    auto. fun_ext. rewrite v_nth_Sn. f_equal. induction x1;auto.
Qed.

Lemma split_equiv: forall (m n : nat) (d : data) (e : exp (ary '{ m * n} d)) (a : path),
  acc' a |:= split e = splitAcc (acc' a) |:= e.
Proof.
  simpl. autounfold. simpl. induction m;auto. induction n. simpl. unfold skip,seq. intros. fun_ext. rewrite seqfor_mul_0,seqfor_no_change. auto.
  intros. rewrite seqfor_nested. unfold seqfor,parfor,split,splitAcc,idx,idxAcc.
  f_equal. fun_ext. repeat f_equal. rewrite ?v_nth_mk_vec;auto. f_equal. autorewrite with core;auto. apply Nat.div_lt_upper_bound;auto.
  rewrite Nat.mul_comm. induction x;auto. induction x;auto. autorewrite with core. apply Nat.mod_upper_bound;auto.
  induction x;auto. apply Nat.div_lt_upper_bound;auto. rewrite Nat.mul_comm. induction x;auto. apply Nat.mod_upper_bound;auto.
  induction x;auto. assert (x < S m * S n)%nat. induction x;auto.
  assert (x / S n < S m)%nat. apply Nat.div_lt_upper_bound;auto. rewrite Nat.mul_comm; induction x;auto.
  assert (x mod S n < S n)%nat. apply Nat.mod_upper_bound;auto.
  assert (x / S n * S n + x mod S n = x)%nat. rewrite Nat.mul_comm. rewrite <- Nat.div_mod with(y:=S n);auto.
  rewrite ?v_nth_mk_vec;autorewrite with core;auto.
  autorewrite with core;try (rewrite H2);auto.
Qed.

Lemma join_equiv: forall (n m : nat) (d : data) (e : exp (ary '{ m} (ary '{ n} d))) (a : path),
  acc' a |:= join e = joinAcc (acc' a) |:= e.
Proof.
  simpl. autounfold. simpl. induction m;auto. induction n. simpl. intros. unfold skip,seq. fun_ext. rewrite seqfor_mul_0,seqfor_no_change. auto.
  intros.  rewrite seqfor_nested. unfold join,joinAcc,idx,idxAcc. f_equal. fun_ext.
  assert (x < S m * S n)%nat. induction x;auto. assert (x / S n < S m)%nat.
  apply Nat.div_lt_upper_bound;auto. rewrite Nat.mul_comm; induction x;auto.
  assert (x mod S n < S n)%nat. apply Nat.mod_upper_bound;auto.
  assert (x / S n * S n + x mod S n = x)%nat. rewrite Nat.mul_comm. rewrite <- Nat.div_mod with(y:=S n);auto.
  rewrite ?v_nth_mk_vec;autorewrite with core;auto. f_equal. 
  rewrite (Nat.mul_comm (x/S n) (S n)). rewrite <- Nat.div_mod with(y:= S n);auto.
  autorewrite with core;auto; rewrite H2;auto.
  autorewrite with core;auto;autorewrite with core; try (rewrite H2);auto.
  rewrite H2;auto. autorewrite with core;auto;autorewrite with core; try (rewrite H2);auto.
Qed.

Lemma reducel_equiv2_aux: forall d2 d1 x p0 f e i eta ,
  seqfor (fun (i0 : fin x) (eta0 : env) =>
    (acc' p0 |:= f (v_nth (exp_default d1) e i0) (vrd eta0 (acc' p0)))eta0 ) ((acc' p0 |:= i) eta) 
  = (acc' p0 |:= (@v_reduce (exp d1) (exp d2) x f i e)) eta.
Proof.
  induction x,e;auto. intros. autorewrite with core. unfold seq.
  induction x. simpl. unfold skip. rewrite vrd_assign,path_eqb_refl.
  rewrite assign_assign,path_eqb_refl. auto.
  replace (fun (i0 : fin (S x)) (eta0 : env) => (acc' p0 |:= f
    (@v_nth (exp d1) (S (S x)) (exp_default d1) (v, e) (fin2finS i0))
    (vrd eta0 (acc' p0))) eta0)
  with (fun (i0 : fin (S x)) (eta0 : env) => (acc' p0 |:= f
    (v_nth (exp_default d1) v (fin2finS i0)) (vrd eta0 (acc' p0))) eta0).
  rewrite IHx. rewrite ?vrd_assign,path_eqb_refl.
  rewrite v_nth_x. rewrite assign_assign,path_eqb_refl.
  simpl v_reduce. auto. repeat fun_ext. rewrite v_nth_Sn.
  auto. induction x0;auto.
Qed. 

Lemma reducel_equiv2:forall (n : nat) (d1 d2 : data) (f : exp d1 -> exp d2 -> exp d2) 
  (i : exp d2) (e : exp (ary '{ n} d1)) (c : exp d2 -> comm) (a:path),
  (forall e e1 x, c e1 (((@acc' d2  a) |:= e) x) = ((@acc' d2 a)|:= e) (c e1 x)) ->
  c (reduce f i e) =
  new (fun ac => ac |:= i '; seqfor (fun (i0 : fin n) eta => 
    (ac |:= f e |[ i0] (vrd eta ac)) eta) '; (fun eta => c (vrd eta ac) eta)) (acc' a).
Proof.
  autounfold. simpl. intros. fun_ext.
  rewrite reducel_equiv2_aux. rewrite H.
  rewrite vrd_assign,path_eqb_refl. rewrite vrm_assign;auto.
Qed.



